(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const i2 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const v10 Bool)
(assert v6)
(assert (xor v6 v0 v5 v7 v8))
(declare-const v11 Bool)
(declare-const v12 Bool)
(assert (xor v10 v7 v3 v2 (= 78 (abs i6)) v11 v8))
(assert (=> v2 v5))
(assert v7)
(declare-const v13 Bool)
(assert (or v7 v12))
(assert (xor (= (* (abs i6) (- (abs i5)) (abs i6)) i6) v1 (or v11 v8 v7 v3 (xor v6 v0 v5 v7 v8) v6 (< 76 54)) (xor v6 (< 76 54) v7 v4 v10 (< i6 39) v6 (< 76 54)) (=> v2 v5) (xor v10 v7 v3 v2 (= 78 (abs i6)) v11 v8) (or v11 v8 v7 v3 (xor v6 v0 v5 v7 v8) v6 (< 76 54))))
(assert (not (distinct (= i5 i6) v10)))
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert (and (= 78 (abs i6)) (or v7 v12) (> (* (abs i6) (- (abs i5)) (abs i6)) (mod i2 i5)) v5 (or v7 v12) v3 (xor (= (* (abs i6) (- (abs i5)) (abs i6)) i6) v1 (or v11 v8 v7 v3 (xor v6 v0 v5 v7 v8) v6 (< 76 54)) (xor v6 (< 76 54) v7 v4 v10 (< i6 39) v6 (< 76 54)) (=> v2 v5) (xor v10 v7 v3 v2 (= 78 (abs i6)) v11 v8) (or v11 v8 v7 v3 (xor v6 v0 v5 v7 v8) v6 (< 76 54)))))
(assert v3)
(declare-const i8 Int)
(declare-const i9 Int)
(assert v9)
(declare-const v16 Bool)
(declare-const v17 Bool)
(assert v13)
(check-sat)
